COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.SEC(Predicate Calculus)
C00016 00003	%7LEMMA 3%1   If ?B does not depend upon ?A in a deduction ?G,?A%5ε%1?B, then
C00021 ENDMK
C⊗;
.SEC(Predicate Calculus)
.SS(The Deductive System)
.BEGIN NOFILL;
%21%1.  Countable set of symbols
	auxiliary symbols: ~, ⊃, ∀, (, ), ,.
	variables (denumerably many): x, ?x1, ?x2, ..., ?xn, ..., ?y1, ?y2, ..., ?yn, ...
	constants (countably many,≥0): ?a, ?a1, ?a2, ..., ?an, ..., %db, b%41%1, ...
	predicate letters (countably many, ≥1):%d A, A%41%d, A%42%1, ..., %dB, B%41%d, B%42%1,...
	function letters (countably many, ≥0): %df, f%41%d, f%42%1, ...,  %dg%1,...
.END
The subscript on predicate and function letters is just an indexing number
to distinguish different predicates and functions.  There are function
and predicate letters which take n arguments for any value of n, this is
not indicated in the letters themselves but will be obvious when they
appear in context.  Thus the unary function letter in %df%1(?x) has absolutely
no relation to the binary function letter in %df%1(?x,?y).

%22%1.  The function letters applied to variables and constants generate 
the %3terms%1:
.begin nofill
	<term>:=<variable> | <constant> | <function letter>(<term>%41%1,...,<term>%4n%1)
The predicate letters applied to terms yield the %3atomic formulas%1:
	<atomic formula>:= <predicate letter>(<term>%41%1,...,<term>%4n%1)
A well-formed formula (wff) is defined as follows:
	<wff>:=<atomic formula> | ~<wff> | <wff>⊃<wff> | ((∀<variable>)<wff>)
.end

In ((∀?y)?A), "?A" is the %3scope%1 of the quantifier (∀?y).  "(∀?y)" is the
%3universal quantifier%1.  ((∀?y)?A) means that for all ?y, property ?A holds.
If ?A does not contain the variable ?y, we take ((∀?y)?A) to mean the same
as ?A.  "∃" is the %3existential quantifier%1.  ((∃?y)?A)) means that there
exists some ?y such that ?A holds.  It was unnecessary to make "∃" a
primitive symbol since we can define it as follows:

.BEGIN center;
	(∃?x)?A stands for ~((∀?x)~?A)
.END
The symbols ∧, and ∨ are defined as for L.  We use the same conventions as
before for eliminating parentheses with the additional convention that
the quantifiers (∀?y) and (∃?y) rank between ⊃, and ∨, ∧, ~.  We also omit 
parentheses around quantified formulas when they are preceded by other
quantifiers.

.BEGIN center;
ex. (∀?x1)(∃?x4)%dA%41%1(?x1,?x2,?x4) stands for ((∀?x1)((∃?x4)%dA%41%1(?x1,?x2,?x4)))

.END
An occurrence of a variable ?x is %3bound%1 in a wff iff it is either the 
variable of a quantifier, "(∀?x)" or "(∃?x)" in the wff, or it is the same variable
that is quantified and within the scope of the quantifier.  Otherwise the
occurrence is said to be %3free%1 in the wff.
A variable may have both bound and free occurrences in a given wff.  Also,
an occurrence of a variable may be bound in a wff ?A, and free in some 
subformula of ?A.  A variable is said to be %3free (bound)%1 in a wff
iff it has a free (bound) occurrence in the wff.  Thus a variable may be 
both bound and free in the same wff.

.BEGIN center;

		ex.  %dA%41%1(?x1,?x2)⊃(∀?x1)%dA%41%1(?x1)
	The first occurrence of ?x1 is free, the second and third are bound.
.END
We shall often indicate that a wff ?A has some of the free variables ?x1, ..., ?xk
by writing it as ?A(?x1,...,?xk).  This does not mean that ?A contains 
precisely these variables as free variables.  It is simply convenient 
notation as then we agree to write ?A(?t1, ..., ?tk) as the result of
substituting the terms ?t1, ..., ?tk for all the free occurrences (if any) of
?x1#,...,#?xk, respectively.  The different script should make clear the difference
between ?A(?x1,...,?xk) just defined, and %dA%1(?x1,...,?xk) which is a
predicate with precisely k arguments ?x1, ..., ?xk.
.R7:
If ?A is a wff and ?t is a term, then ?t is said to be %3free for ?xi%3 in ?A
iff no free occurrences of ?xi in ?A lie within the scope of any quantifier
(∀?xj) where ?xj is a variable in ?t.

.BEGIN NOFILL;
	exs. 1) ?x2 is free for ?x1 in %dA%41%1(?x1), but is not free for ?x1 in (∀?x2)%dA%41%1(?x1).
	     2) Any term ?t containing no variables is free for any variable in any wff.
	     3) A term ?t is free for any variable in ?A if none of the variables of ?t is bound in ?A.
.END

.P7:
%23%1.  The following axiomatization of Predicate Calculus is due to Mendelson[##].
If ?A,?B,?C are wffs⊗↓in this chapter all wffs are assumed to be such in the
Theory of Predicate Calculus as that is the only theory under discussion←, then
the following are axioms:

.BEGIN NOFILL; group;      
		%7A1%1:     ?A⊃(?B⊃?A)
		%7A2%1:     (?A⊃(?B⊃?C)) ⊃ ((?A⊃?B)⊃(?A⊃?C))
		%7A3%1:     (~?B⊃~?A) ⊃ ((~?B⊃?A)⊃?B)
		%7A4%1:     (∀?xi)?A(?xi)⊃?A(?t), if ?A(?xi) is a wff and ?t is a term free for ?xi in ?A(?xi).
			    (Note that if ?t is ?xi we have the axioms (∀?xi)?A(?xi)⊃?A(?xi).
		%7A5%1:     (∀?xi)(?A⊃?B) ⊃ (?A⊃(∀?xi)?B) if ?A is a wff containing no free occurrences of ?xi.
.END
Note that the first three axioms are just those used for L in the last chapter,
we have added two more since we now have variables and quantifiers to worry about.


%24.%1   We have two rules of inference for Predicate Calculus (henceforth PC):

.BEGIN NOFILL;
		Modus Ponens (%7MP%1):  ?B follows from ?A and ?A⊃?B
		Generalization (%7Gen%1):  (∀?x)?A follows from ?A.
.END

An %3instance%1 of a statement form is a wff obtained from the statement form
by substituting wffs for all statement letters, all occurrences of the same 
statement letter being replaced by the same wff.

.begin group
%7LEMMA 1%1  Every wff ?A which is an instance of a tautology is a theorem, and it 
may be proved using only Axioms %7A1-A3%1 and %7MP%1.
Proof:
.BEGIN indent 15,10;
?A arises from a tautology %eP%1 by substitution.  By completeness for L, there
is a proof of %eP%1 in L.  In such a proof, make the same substitutions of wffs
of PC for the proposition letters as were used in obtaining ?A from %eP%1, and
for all proposition letters in the proof which do not occur in %eP%1, substitute
an arbitrary wff of PC.
The resulting sequence of wffs is a proof of ?A, and this proof uses only 
%7A1-A3%1 and %7MP%1.
.end
.end

%7LEMMA 2%1  Predicate Calculus is consistent.
.BEGIN NOFILL;
Proof:
.begin fill indent 10,10;
	For each wff ?A, let ?h(?A) be the expresion obtained by deleting all quantifiers and terms in ?A
.begin nofill;
	   ex. ?h(~(∀?x1)%dA%41%1(?x1,?x2)⊃%dA%42%1(?x3)) = (~%dA%41%1⊃%dA%42%1).
.end
	Then ?h(?A) is a wff of L with the symbols %dA%4j%1 as proposition letters.
	Clearly, ?h(~?A)=~(?h(?A)) 
	    and  ?h(?A⊃?B)=?h(?A)⊃?h(?B).
	For every axiom ?A given by %7A1-A5%1, ?h(?A) is a tautology. For %7A1-A3%1, this is obvious.

	%7A4%1: An instance of (∀?xi)?A(?xi)⊃?A(?t), under ?h is transformed into a tautology of the form ?A⊃?A

	%7A5%1: An instance of (∀?xi)(?A⊃?B)⊃(?A⊃(∀?xi)?B) becomes (?A⊃?B)⊃(?A⊃?B).

	Also, if ?h(?A) and ?h(?A⊃?B) are tautologies, then by Lemma 6 ({yonss(P9)},{yon(P8)}), so is ?h(?B);and
	if ?h(?A) is a tautology so is ?h((∀?xi)?A) which is just ?h(?A).
	Hence ?h(?A) is a tautology whenever ?A is a theorem of PC.

	If there were a wff ?B such that %5ε%1?B and %5ε%1~?B then both ?h(?B) and ?h(~?B)=~?h(?B)
	would be tautologies, which is impossible.

	%5.%1 PC is consistent.
.end
.END

The deduction theorem of L requires modification for statement in
PC.
.BEGIN NOFILL;
		ex. For any wff ?A, ?A%5ε%1(∀?x)?A, but it is not always the case that %5ε%1?A⊃(∀?x)?A.
		Let ?A be ?x≠0.
		By applying ?Gen we get ?x≠0%5ε%1(∀?x)?x≠0
		and by substitution (∀?x)?x≠0%5ε%10≠0
		however, we cannot prove ?x≠0 ⊃ (∀?x)?x≠0
		i.e., we cannot get %5ε%1?x≠0 ⊃ 0≠0
.END

Let ?A be a wff in a set ?G of wffs; assume we are given a deduction
?B1,...,?Bn from ?G, together with justification for each step of the 
deduction.  We say that ?Bi %3depends upon%1 ?A in this proof iff
.BEGIN INDENT 10,10,;

1) ?Bi is ?A and the justification for ?Bi is that it belongs to ?G; or

2) ?Bi is justified as a direct consequence by ?MP or ?Gen of some preceding
wffs of the sequence, where at least one of the preceding wffs depends upon
?A
.END

.BEGIN NOFILL;
			ex.  (∀?x1)?A⊃?C %5ε%1(∀?x1)?C
			  ?B1:	?A		hyp
			  ?B2:	(∀?x1)?A	?B1,?Gen
			  ?B3:	(∀?x1)?A⊃?C	hyp
			  ?B4:	?C		?B2,?B3, ?MP
			  ?B5:	(∀?x1)?C	?B4,?Gen
			?B1 depends upon ?A
			?B2 depends upon ?A
			?B3 depends upon (∀?x1)?A⊃?C
			?B4 depends upon ?A and (∀?x1)?A⊃?C
			?B5 depends upon ?A and (∀?x1)?A⊃?C
.END







%7LEMMA 3%1   If ?B does not depend upon ?A in a deduction ?G,?A%5ε%1?B, then
?G%5ε?B.
.BEGIN NOFILL;
Proof:
.end
.BEGIN INDENT 10,10;
Let ?B1, ..., ?Bn=?B be a deduction of ?B from ?G and ?A, in which ?B does not
depend upon ?A.  

If n=1, then ?B1=?B which does not depend upon ?A, %5.%1 ?Bε?G, or ?B is an
axiom, %5.%1 ?G%5ε%1?B

Assume true for n<k. If ?B belongs to ?G or is an axiom, then ?G%5ε%1?B.
If ?B is a direct consequence of one or two preceding wffs, then, since
?B does not depend upon ?A, neither do these preceding wffs.  By the 
inductive hypothesis these preceding wffs are deducible from ?G alone,
%5.%1 so is ?B.
.END


%7THEOREM 4%1 (Deduction theorem for PC)
    Assume that ?G,?A %5ε%1?B, where in the deduction, no application of
?Gen to a wff which depends upon ?A has as its quantified variable a free
variable of ?A. Then ?G%5ε%1?A⊃?B
.BEGIN NOFILL;
Proof:
.END	
.BEGIN INDENT 5,5;
Let ?B1, ..., ?Bn=?B be a deduction of ?B from ?G,?A satisfying the assumption
of the theorem. We shall show by induction on i, that ?G%5ε%1?A⊃?Bi for each
i≤n.
.end
.begin NOFILL;      
.group
	i=1: 1) ?Bi is an axiom or belongs to ?G.  
	        Then ?G%5ε%1?Bi
		?Bi⊃(?A⊃?Bi)    axiom %7A1%1
		%5.%1 ?G%5ε?A⊃?Bi     by ?MP
	     2) ?Bi is ?A
		%5ε%1?A⊃?A     by lemma 2 of {yonss(P10)},{yon(P11)};
		%5.%1 ?G%5ε%1?A⊃?Bi
.apart;
.group;
	assume theorem for i<k:
	     1) ?Bk is an axiom or an element of ?G
		true by case 1) above.
	     2) ?Bk is ?A
		true by case 2) above.
	     3) ?Bk follows by ?MP from ?Bi and ?Bj=?Bi⊃?Bk, i,j<k
		?G%5ε%1?A⊃?Bi		induction hyp
		?G%5ε%1?A⊃(?Bi⊃?Bk)	induction hyp
		%5ε%1(?A⊃(?Bi⊃?Bk)) ⊃ ((?A⊃?Bi)⊃(?A⊃?Bk))	%7A2%1
		%5.%1 ?G%5ε%1?A⊃?Bk	?MP
.apart
.group
	     4) ?Bk follows by ?Gen from ?Bj, j<k
		?G%5ε%1?A⊃?Bj		induction hyp
		    a)	?Bj does not depend upon ?A
			?G%5ε%1?Bj	Lemma 3
			?G%5ε%1(∀?x)?Bj  i.e.,?G%5ε%1?Bk	?Gen
			%5ε%1?Bk⊃(?A⊃?Bk)	%7A1%1
			%5.%1 ?G%5ε%1?A⊃?Bk	?MP
		    b)  ?x is not a free variable of ?A
			%5ε%1(∀?x)(?A⊃?Bj)⊃(?A⊃(∀?x)?Bj)	%7A5%1
			?G%5ε%1?A⊃?Bj		by induction hyp
			?G%5ε%1(∀?x)(?A⊃?Bj)	?Gen
			?G%5ε%1?A⊃(∀?x)?Bj	?MP
			i.e., ?G%5ε%1?A⊃?Bk
	The theorem follows as the case where i=n.
.END

The hypothesis of the deduction theorem for PC is cumbersome, the following
corollaries are more transparent and often more useful.

%7Corollary 4.1%1  If a deduction ?G,?A%5ε%1?B involves no application of ?Gen 
in which the quantified variable is free in ?A, then ?G%5ε?A⊃?B.

%7Corollary 4.2%1  If ?A is closed (contains no free variables) and ?G,?A%5ε%1?B,
then ?G%5ε%1?A⊃?B.

Note:  In the proof of the deduction theorem for PC, ?Bj depends upon a premiss
?C of ?G in the original proof iff ?A⊃?Bj depends upon ?C in the new proof.
This conclusion is useful when we wish to apply the Deduction Theorem
several times in a row to a given deduction, e.g., to obtain
?G%5ε%eD%1⊃(?A⊃?B) from ?G,%eD%1,?A%5ε%1?B.